\begin{frame}
\frametitle{Generating Constraints}

\begin {itemize}\item SQL code and
Number of rows of each related table
$\rightarrow$ Symbolic database instance
\end{itemize}

\cod{CREATE TABLE grades (ID int, grade int);}\\

  \begin{tabular}{|c|c|}
    \hline
    \textbf {ID} & \textbf {grade} \\
    \hline
    grades.ID.0 & grades.grade.0 \\
    grades.ID.1 & grades.grade.1 \\
    \hline
  \end{tabular}\\

 Each symbolic variable has an associated type

\end{frame}
\begin{frame}
Let $D$ be a database schema and $d$ a  database instance. We define $\theta(R,d)$ for every relation $R$ in $D$ as a multiset of pairs $(\psi,\mu)$ with
$\psi$ a first order formula, and $\mu$ a row.\\


\begin{theorem} \label{theo}
Let $D$ be a database schema and $d$ a valid database instance. Let $R$ be either a relation in $D$ or a query defined using relations in $D$.
Then $\eta \in \SQL{R,d}$ with cardinality $k$  iff $(true,\eta) \in \theta(R,d)$ with cardinality $k$.

\end{theorem}
\end{frame}

\begin{frame}{Generating Constraints: Tables}
For every table $T$ in $D$ such that $d(T)=\multi{\mu_1,\dots,\mu_n}$:
where $\mu_i$ = $(T.C_1 \mapsto X_{i1},\dots,T.C_m \mapsto X_{im})$ then:
  $\theta(T,d) = \multi{ (true,\mu_1), \dots, (true,\mu_n) }$.

Considering $\SQL{T,d} = d(T) = \multi{\mu_1 \dots \mu_n}$ it is easy to check that each element $\eta \in d(T)$ is in $\SQL{T,d}$ with cardinality k iff $(true,\eta) \in \theta(R,d)$ with cardinality $k$.
\begin{block}{$\theta(Grades,d)$}

$(true, (grades.ID \mapsto grades.ID.0,grades.grade \mapsto grades.grade.0)),$

$(true,(grades.ID \mapsto grades.ID.1,grades.grade \mapsto grades.grade.1))$
\end{block}

\end{frame}

\begin{frame}{Generating Constraints: Queries}

 {\small If $Q$ is a query: ${\sf select } \ e_1, \dots, e_n \  {\sf from }\ R_1\ B_1 , \dots, R_m \ B_m\  \textrm{\sf where}\ C_w$;\\
Then:
\begin{description}
  \item[$\theta(Q,d)$]$ =  \multileft{ (\psi_1 \wedge \dots \wedge \psi_m \wedge \ftx{C_\mu}{d},\,s_Q(\mu))\ \mid } $\\
 $ (\psi_1, \nu_1) \in \theta(R_1,d), \dots, (\psi_m, \nu_m) \in \theta(R_m,d),  \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}   \multiright$
  where
   \item[$s_Q(\mu)$] = $\{Q.A_1 \mapsto (e_1 \mu), \dots, Q.A_n \mapsto (e_n \mu) \}$,
\end{description}
}
{\small \begin{tabular}{c|c|c}
\textbf{Condition Type}&\textbf{$\SQL{C,d}$} & \textbf{$\ftx{C}{d}$}\\
\hline
\textbf{false} & $\bot$ & $\bot$ \\
\textbf{true} & $\top$ & $\top$ \\
\textbf{Arithmetic expression e} & $e$ & $e$\\
\textbf{$e_1 \diamond e_2$} & $(\SQL{e_1,d} \diamond \SQL{e_2,d})$ & $(\ftx{e_1}{d} \diamond \ftx{e_2}{d})$\\
\textbf{$ C_1\ \cod{ and }\ C_2$} & $ \SQL{C_1,d} \wedge \SQL{C_2,d}$ & $ \ftx{C_1}{d} \wedge \ftx{C_2}{d}$  \\
\textbf{$ C_1\ \cod{ or }\ C_2$} &  $ \SQL{C_1,d} \vee \SQL{C_2,d}$  & $ \ftx{C_1}{d} \vee \ftx{C_2}{d}$  \\
\textbf{not $C$} &  $\neg \SQL{C,d}$ & $\neg \ftx{C}{d}$\\ 
\textbf{Exists $Q$} & $ \SQL{Q, d} \neq \emptyset$ & \begin{tabular}{c} $(\vee_{j=1}^{p} \psi_j)$    having \\$\theta(Q,d) = \multileft (\psi_1, \mu_1),$\\$ \dots (\psi_{p},\mu_{p}) \multiright$.\\ \end{tabular}
\end{tabular}}
\end{frame}

\begin{frame}
\begin{description}
\item[$\theta(Q,d)$] $=  \multileft{ (\psi_1 \wedge \dots \wedge \psi_m \wedge \ftx{C_\mu}{d},\,s_Q(\mu))\ \mid } $\\
 $ (\psi_1, \nu_1) \in \theta(R_1,d), \dots, (\psi_m, \nu_m) \in \theta(R_m,d), $\\$ \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}   \multiright$
\\
\item[$\SQL{Q,d}$] $ = \{ s_Q(\mu) \mid $\\
        $\nu_1 \in \SQL{R_1,d}, \dots, \nu_m \in \SQL{R_m,d},$\\$ \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}, \SQL{C\mu,d} \}$\\
\end{description}

To prove that an element $\eta$ is in $\SQL{Q,d}$ with cardinality $k$ iff $(true,\eta)$ is in $\theta(Q,d)$ with the same cardinality we need to prove
$\SQL{C,d}$ iff $\ftx{C}{d}$ 
\end{frame}

\begin{frame}{Generating Constraints}
\begin{itemize}
\item $\SQL{Q, d}  \neq \emptyset$
\item  $\ftx{C}{d} = (\vee_{j=1}^{p} \psi_j)$. (Being $\theta(Q,d) = \multi{ (\psi_1, \mu_1), \dots (\psi_{p},\mu_{p}) }$) 
\end{itemize}
 $\SQL{Q, d}  \neq \emptyset$ iff there is some $\eta \in \SQL{Q,d}$\\
 iff (applying induction hypothesis) $(true, \eta) \in \theta(Q,d)$\\
 iff $(\vee_{j=1}^{p} \psi_j) = true $ proving  $\SQL{C,d}$ iff $\ftx{C}{d}$

\end{frame}

\begin{frame}
\begin{description}
\item[$\theta(Q,d)$] $=  \multileft{ (\psi_1 \wedge \dots \wedge \psi_m \wedge \ftx{C_\mu}{d},\,s_Q(\mu))\ \mid } $\\
 $ (\psi_1, \nu_1) \in \theta(R_1,d), \dots, (\psi_m, \nu_m) \in \theta(R_m,d), $\\$ \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}   \multiright$
\\
\item[$\SQL{Q,d}$] $ = \{ s_Q(\mu) \mid $\\
        $\nu_1 \in \SQL{R_1,d}, \dots, \nu_m \in \SQL{R_m,d},$\\$ \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}, \SQL{C\mu,d} \}$\\
\end{description}
%{\small
%Once we have proved $\SQL{C,d}$ iff $\ftx{C}{d}$ lets see that  $(true,\eta) \in \theta(Q,d)$ with cardinality k iff $\eta \in \SQL{Q,d}$ with cardinality $k$.

%$(true,\eta) \in \theta(Q,d)$ with cardinality k iff:
%}
%{\small
%\begin{enumerate}
%\item $\mu_i =  {\nu^i_1}^{B_1} \odot \cdots \odot {\nu^i_m}^{B_m}, \textrm{ for some }  (\psi^i_1, \nu^i_1) \in \theta(R_1,d), \dots, (\psi^i_m, \nu^i_m) \in \theta(R_m,d)$ \label{demo:eq:mudef} \\
%\item $\eta  = s_Q(\mu_i)$   \label{demo:eq:etadef} \\
%\item $\psi^i_1=true, \dots,  \psi^i_m=true$ \label{demo:eq:psitrue} \\
%\item $\ftx{C\mu}{d}=true \textrm{ and thus } \SQL{C\mu,d}=true $ \label{demo:eq:C'true}
%\end{enumerate}
% }
\end{frame}

\subsection{Test Case}
\begin{frame}{Generating Constraint: Test Case}

\begin{corollary} \label{coro}
Let $D$ be a database schema and $d_s$ a symbolic database instance.
Let $R$ be a relation in $D$
such that $\theta(R) = \multi{ (\psi_1, \mu_1), \dots (\psi_n,\mu_n) }$,
and $\eta$ a substitution satisfying  $d_s$.
Then $d_s\eta$ is a PTC for $R$ iff
$(\bigvee_{i=1}^n \psi_i)\eta = true$.
\end{corollary}
\begin{proof}
Straightforward from Theorem \ref{theo}:  $(\bigvee_{i=1}^n \psi_i)\eta = true$ iff
there is some $\psi_i$ with $1 \leq i \leq n$ such that $\psi_i\eta = true$ iff
 $(\mu_i\eta) \in \SQL{R}$ iff  $\SQL{R} \neq \emptyset$.
\end{proof}

\end{frame}